postulate
  ℕ   : Set
  _+_ : ℕ → ℕ → ℕ
  foo : ℕ → ℕ

{-# DISPLAY foo (x + x) = x #-}
